<html>
<head><meta charset="utf-8"><title>meeting 2019-10-21 · wg-traits · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/index.html">wg-traits</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html">meeting 2019-10-21</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="178672663"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178672663" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178672663">(Oct 21 2019 at 16:31)</a>:</h4>
<p>Hey <span class="user-group-mention" data-user-group-id="692">@WG-traits</span> -- </p>
<p>So do we want to have a design meeting today? It hasn't been long since our last one, and I was traveling much of that time, so I didn't have time to "prepare" anything. However, here are some things I think we could talk about:</p>
<ul>
<li>rustc: lazy normalization for associated constants. I've been toying with a scheme and what that might mean.</li>
<li>rustc: upcasting. We could talk over the work <span class="user-mention" data-user-id="124069">@Alexander Regueiro</span> has been doing and (perhaps) what else needs to be done to round out that effort.</li>
<li>chalk: specialization. Trying to get synched back up on the work we were doing here (sorry <span class="user-mention" data-user-id="117350">@Sunjay Varma</span>!) and figure out concrete steps.</li>
<li>region constraints in chalk / polonius: I have thoughts about how these should work, albeit mildly out of cache</li>
<li>other topics? I'm open to proposals.</li>
</ul>
<p>I'm going to go for a bit but I'll see what people think when I get back =)</p>



<a name="178673289"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178673289" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178673289">(Oct 21 2019 at 16:38)</a>:</h4>
<p>Sounds fair</p>



<a name="178673302"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178673302" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178673302">(Oct 21 2019 at 16:38)</a>:</h4>
<p>I can make tonight for once!</p>



<a name="178673692"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178673692" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Sunjay Varma <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178673692">(Oct 21 2019 at 16:42)</a>:</h4>
<p>I will probably be in another meeting today at 2 pm, but yes very excited to start on specialization again!</p>



<a name="178678770"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178678770" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178678770">(Oct 21 2019 at 17:39)</a>:</h4>
<p>Some other possible topics I thought of later:</p>
<ul>
<li>talking over the strategy on <code>dyn Trait</code> and chalk integration (cc <span class="user-mention" data-user-id="116108">@Keith Yeung</span>)</li>
<li>the soundness hole around coherence and <code>dyn Trait</code> values (cc <span class="user-mention" data-user-id="128294">@blitzerr</span>)</li>
</ul>



<a name="178678858"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178678858" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178678858">(Oct 21 2019 at 17:40)</a>:</h4>
<p>or maybe:</p>
<ul>
<li>meta-meeting to discuss planning and chart out some topics for the next few meetings :)</li>
</ul>



<a name="178681356"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178681356" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178681356">(Oct 21 2019 at 18:04)</a>:</h4>
<p>OK, <span class="user-group-mention" data-user-group-id="692">@WG-traits</span> hello =)</p>



<a name="178681500"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178681500" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178681500">(Oct 21 2019 at 18:05)</a>:</h4>
<p>So as I wrote above, I'm not 100% sure what to talk about today, but open to suggestions. I mostly just want us to keep talking more than anything. =)</p>



<a name="178681555"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178681555" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178681555">(Oct 21 2019 at 18:06)</a>:</h4>
<p>I guess it depends a bit on who's around</p>



<a name="178681720"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178681720" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178681720">(Oct 21 2019 at 18:08)</a>:</h4>
<p>I think I would probably narrow down to 2 things that seem best to me:</p>
<ul>
<li>discussing the strategy around <code>dyn Trait</code> integration into chalk that <span class="user-mention" data-user-id="116108">@Keith Yeung</span> is working on (I see they're here)</li>
<li>talking about lazy norm and assoc constants a bit</li>
</ul>
<p>All the topics above seem imp't, but I think I'd rather do the "planning" part a bit separately.</p>



<a name="178681835"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178681835" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178681835">(Oct 21 2019 at 18:09)</a>:</h4>
<p>OK, let's just start in on the first one a bit</p>



<a name="178681888"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178681888" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178681888">(Oct 21 2019 at 18:09)</a>:</h4>
<p>The basic problem is that Chalk doesn't understand anything about <code>dyn Trait</code> -- or didn't</p>



<a name="178682020"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178682020" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178682020">(Oct 21 2019 at 18:10)</a>:</h4>
<p><span class="user-mention" data-user-id="116108">@Keith Yeung</span> added a new sort of type for that (<a href="https://github.com/rust-lang/chalk/blob/8abd14e1f0bb65dc95fdbbb87c12a95cc0063da1/chalk-ir/src/lib.rs#L238-L245" target="_blank" title="https://github.com/rust-lang/chalk/blob/8abd14e1f0bb65dc95fdbbb87c12a95cc0063da1/chalk-ir/src/lib.rs#L238-L245">link</a>)</p>



<a name="178682035"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178682035" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178682035">(Oct 21 2019 at 18:10)</a>:</h4>
<p>It looks like this:</p>
<div class="codehilite"><pre><span></span><span class="w">    </span><span class="sd">/// A &quot;dyn&quot; type is a trait object type created via the &quot;dyn Trait&quot; syntax.</span>
<span class="w">    </span><span class="sd">/// In the chalk parser, the traits that the object represents is parsed as</span>
<span class="w">    </span><span class="sd">/// a QuantifiedInlineBound, and is then changed to a list of where clauses</span>
<span class="w">    </span><span class="sd">/// during lowering.</span>
<span class="w">    </span><span class="sd">///</span>
<span class="w">    </span><span class="sd">/// See the `Opaque` variant for a discussion about the use of</span>
<span class="w">    </span><span class="sd">/// binders here.</span>
<span class="w">    </span><span class="n">Dyn</span><span class="p">(</span><span class="n">Binders</span><span class="o">&lt;</span><span class="nb">Vec</span><span class="o">&lt;</span><span class="n">QuantifiedWhereClause</span><span class="o">&gt;&gt;</span><span class="p">),</span><span class="w"></span>
</pre></div>



<a name="178682053"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178682053" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178682053">(Oct 21 2019 at 18:11)</a>:</h4>
<p>(I'm going to skip past <code>impl trait</code> for a section, but we can loop back to that)</p>



<a name="178682099"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178682099" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178682099">(Oct 21 2019 at 18:11)</a>:</h4>
<p>This type definition is sort of interesting I think because it looks very different from other types; it embeds "where clauses"</p>



<a name="178682207"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178682207" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178682207">(Oct 21 2019 at 18:12)</a>:</h4>
<p>this comes back to the idea of <code>dyn Trait</code> being a kind of "existential type" -- i.e., shorthand for a type like <code>exists&lt;T&gt; { T: Trait }</code>. i.e., "some type that implements <code>Trait</code>"</p>



<a name="178682225"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178682225" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178682225">(Oct 21 2019 at 18:12)</a>:</h4>
<p>(make sense so far?)</p>



<a name="178682284"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178682284" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178682284">(Oct 21 2019 at 18:13)</a>:</h4>
<p>I thought that was a bit odd, but guess it makes sense if you do <code>Self: Trait</code></p>



<a name="178682389"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178682389" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178682389">(Oct 21 2019 at 18:14)</a>:</h4>
<p>(my internet is flaking so sorry if this comes out of order)</p>



<a name="178682479"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178682479" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178682479">(Oct 21 2019 at 18:15)</a>:</h4>
<p>Not sure about the <code>Self</code>, but the <code>exists</code> makes sense</p>



<a name="178682491"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178682491" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178682491">(Oct 21 2019 at 18:15)</a>:</h4>
<p>(er, sorry! afk for 2 minutes)</p>



<a name="178682569"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178682569" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178682569">(Oct 21 2019 at 18:16)</a>:</h4>
<p>yeah nevermind, the <code>Self</code> part doesn't seem right</p>



<a name="178682599"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178682599" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178682599">(Oct 21 2019 at 18:16)</a>:</h4>
<p>I sent that before niko's better explanation ;)</p>



<a name="178682863"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178682863" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178682863">(Oct 21 2019 at 18:19)</a>:</h4>
<p>ok, back</p>



<a name="178682884"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178682884" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178682884">(Oct 21 2019 at 18:19)</a>:</h4>
<p>I'm not sure what you meant by <code>Self</code> but</p>



<a name="178682893"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178682893" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178682893">(Oct 21 2019 at 18:19)</a>:</h4>
<p>I guess that worked out :)</p>



<a name="178682899"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178682899" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178682899">(Oct 21 2019 at 18:19)</a>:</h4>
<p>in any case, I think the binders etc there are interesting</p>



<a name="178682940"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178682940" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178682940">(Oct 21 2019 at 18:19)</a>:</h4>
<div class="codehilite"><pre><span></span><span class="n">Binders</span><span class="o">&lt;</span><span class="nb">Vec</span><span class="o">&lt;</span><span class="n">QuantifiedWhereClause</span><span class="o">&gt;&gt;</span><span class="p">)</span><span class="w"></span>
</pre></div>


<p>kind of expands to</p>
<div class="codehilite"><pre><span></span><span class="n">Binders</span><span class="o">&lt;</span><span class="nb">Vec</span><span class="o">&lt;</span><span class="n">Binders</span><span class="o">&lt;</span><span class="n">WhereClause</span><span class="o">&gt;&gt;&gt;</span><span class="w"></span>
</pre></div>



<a name="178683015"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683015" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683015">(Oct 21 2019 at 18:20)</a>:</h4>
<p>the notation <code>exists&lt;T&gt; { T: Trait }</code> -- that <code>exists</code> is the first round of <code>Binders</code></p>



<a name="178683038"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683038" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683038">(Oct 21 2019 at 18:20)</a>:</h4>
<p>the second round is to allow for things like</p>



<a name="178683070"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683070" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683070">(Oct 21 2019 at 18:20)</a>:</h4>
<div class="codehilite"><pre><span></span><span class="n">dyn</span><span class="w"> </span><span class="nb">FnOnce</span><span class="p">(</span><span class="o">&amp;</span><span class="kt">u8</span><span class="p">)</span><span class="w"></span>
<span class="n">dyn</span><span class="w"> </span><span class="k">for</span><span class="o">&lt;</span><span class="na">&#39;a</span><span class="o">&gt;</span><span class="w"> </span><span class="n">Trait</span><span class="o">&lt;</span><span class="na">&#39;a</span><span class="o">&gt;</span><span class="w"></span>
</pre></div>



<a name="178683122"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683122" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683122">(Oct 21 2019 at 18:21)</a>:</h4>
<p>which would correspond to a type like</p>
<div class="codehilite"><pre><span></span>exists&lt;T&gt; { forall&lt;&#39;a&gt; { T: FnOnce&lt;(&amp;&#39;a u8,)&gt; } }
exists&lt;T&gt; { forall&lt;&#39;a&gt; { T: Trait&lt;&#39;a&gt; } }
</pre></div>



<a name="178683142"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683142" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683142">(Oct 21 2019 at 18:21)</a>:</h4>
<p>you can see now where the "inner binders" comes from, maybe</p>



<a name="178683300"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683300" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683300">(Oct 21 2019 at 18:23)</a>:</h4>
<p>ok, any questions on that? (I was pausing, but didn't say so)</p>



<a name="178683314"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683314" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683314">(Oct 21 2019 at 18:23)</a>:</h4>
<p>ok so besides the type def'n</p>



<a name="178683319"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683319" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683319">(Oct 21 2019 at 18:23)</a>:</h4>
<p>how do we integrate these "dyn Trait" types into trait solving?</p>



<a name="178683387"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683387" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683387">(Oct 21 2019 at 18:24)</a>:</h4>
<p>there is an imp't caveat here, which is that we're wrestling with these rules in rustc proper</p>



<a name="178683424"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683424" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683424">(Oct 21 2019 at 18:24)</a>:</h4>
<p>but I'm going to give the simple version to start</p>



<a name="178683449"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683449" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683449">(Oct 21 2019 at 18:25)</a>:</h4>
<p>the basic rule that we want is that <code>dyn Foo: Foo</code> for any <code>Foo</code></p>



<a name="178683475"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683475" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683475">(Oct 21 2019 at 18:25)</a>:</h4>
<p>Hmm, that reminds me, solving for impl Trait is different from dyn Trait</p>



<a name="178683478"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683478" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683478">(Oct 21 2019 at 18:25)</a>:</h4>
<p>this is an implication of a trait being "dyn safe" (which we don't presently choose to model)</p>



<a name="178683504"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683504" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683504">(Oct 21 2019 at 18:25)</a>:</h4>
<blockquote>
<p>Hmm, that reminds me, solving for impl Trait is different from dyn Trait</p>
</blockquote>
<p>hmm, I'm not 100% sure what yo mean but let's come back to that</p>



<a name="178683514"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683514" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683514">(Oct 21 2019 at 18:26)</a>:</h4>
<blockquote>
<p>ok, any questions on that? (I was pausing, but didn't say so)</p>
</blockquote>
<p>it's been awhile since I worked in chalk, but I thought <code>Binders</code> only corresponded to <code>forall</code> quantifiers</p>



<a name="178683568"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683568" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683568">(Oct 21 2019 at 18:26)</a>:</h4>
<p>no, Binders correspond to any sort of quantifier; whether it is forall or exists comes from the surrounding context</p>



<a name="178683596"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683596" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683596">(Oct 21 2019 at 18:26)</a>:</h4>
<p>Maybe only one of them was used initially in Chalk?</p>



<a name="178683604"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683604" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683604">(Oct 21 2019 at 18:26)</a>:</h4>
<p>okay, I find the docs confusing in that case</p>



<a name="178683610"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683610" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683610">(Oct 21 2019 at 18:27)</a>:</h4>
<blockquote>
<p>Maybe only one of them was used initially in Chalk?</p>
</blockquote>
<p>nope</p>



<a name="178683624"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683624" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683624">(Oct 21 2019 at 18:27)</a>:</h4>
<p>but forall is far more common</p>



<a name="178683650"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683650" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683650">(Oct 21 2019 at 18:27)</a>:</h4>
<p>see e.g. <a href="https://github.com/rust-lang/chalk/blob/8abd14e1f0bb65dc95fdbbb87c12a95cc0063da1/chalk-ir/src/lib.rs#L958" target="_blank" title="https://github.com/rust-lang/chalk/blob/8abd14e1f0bb65dc95fdbbb87c12a95cc0063da1/chalk-ir/src/lib.rs#L958">this part of the <code>Goal</code> definition</a></p>



<a name="178683663"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683663" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683663">(Oct 21 2019 at 18:27)</a>:</h4>
<div class="codehilite"><pre><span></span><span class="w">   </span><span class="n">Quantified</span><span class="p">(</span><span class="n">QuantifierKind</span><span class="p">,</span><span class="w"> </span><span class="n">Binders</span><span class="o">&lt;</span><span class="nb">Box</span><span class="o">&lt;</span><span class="n">Goal</span><span class="o">&gt;&gt;</span><span class="p">),</span><span class="w"></span>
</pre></div>



<a name="178683676"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683676" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683676">(Oct 21 2019 at 18:27)</a>:</h4>
<p>that encodes both <code>forall&lt;T&gt; { .. }</code> and <code>exists&lt;T&gt; { ... }</code> goals</p>



<a name="178683681"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683681" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683681">(Oct 21 2019 at 18:27)</a>:</h4>
<p>I think the best way to thikn about <code>Binders</code> is as the <code>&lt;T&gt; { .. }</code> part</p>



<a name="178683692"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683692" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683692">(Oct 21 2019 at 18:27)</a>:</h4>
<p>without the <code>forall</code> or <code>exists</code></p>



<a name="178683760"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683760" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683760">(Oct 21 2019 at 18:28)</a>:</h4>
<p>for completeness, <a href="https://github.com/rust-lang/chalk/blob/8abd14e1f0bb65dc95fdbbb87c12a95cc0063da1/chalk-ir/src/lib.rs#L1020-L1023" target="_blank" title="https://github.com/rust-lang/chalk/blob/8abd14e1f0bb65dc95fdbbb87c12a95cc0063da1/chalk-ir/src/lib.rs#L1020-L1023"><code>QuantifiedKind</code></a> is:</p>
<div class="codehilite"><pre><span></span><span class="k">pub</span><span class="w"> </span><span class="k">enum</span> <span class="nc">QuantifierKind</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">    </span><span class="n">ForAll</span><span class="p">,</span><span class="w"></span>
<span class="w">    </span><span class="n">Exists</span><span class="p">,</span><span class="w"></span>
<span class="p">}</span><span class="w"></span>
</pre></div>



<a name="178683785"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683785" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683785">(Oct 21 2019 at 18:28)</a>:</h4>
<blockquote>
<p>okay, I find the docs confusing in that case</p>
</blockquote>
<p>that...seems quite likely</p>



<a name="178683796"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683796" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683796">(Oct 21 2019 at 18:28)</a>:</h4>
<p><a href="https://rust-lang.github.io/chalk/chalk_ir/struct.Binders.html" target="_blank" title="https://rust-lang.github.io/chalk/chalk_ir/struct.Binders.html">docs for Binders</a></p>



<a name="178683815"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683815" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683815">(Oct 21 2019 at 18:29)</a>:</h4>
<p>Hmm, why not something like <code>Quantified(QuantifierKind, Binders, Box&lt;Goal&gt;)</code> then?</p>



<a name="178683827"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683827" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683827">(Oct 21 2019 at 18:29)</a>:</h4>
<p><span class="user-mention" data-user-id="125131">@detrumi</span> the <code>Binders&lt;T&gt;</code> encloses the value that is bound</p>



<a name="178683850"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683850" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683850">(Oct 21 2019 at 18:29)</a>:</h4>
<p>this is useful because you often want to have operations like</p>
<div class="codehilite"><pre><span></span><span class="n">instantiate</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="p">(</span><span class="n">x</span>: <span class="kp">&amp;</span><span class="nc">Binders</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="p">)</span><span class="w"> </span>-&gt; <span class="nc">T</span><span class="w"></span>
</pre></div>



<a name="178683863"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683863" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683863">(Oct 21 2019 at 18:30)</a>:</h4>
<p>that will take all the bound variables and replace them with inference variables, returning the <code>T</code> inside</p>



<a name="178683928"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683928" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683928">(Oct 21 2019 at 18:30)</a>:</h4>
<p>it is also useful because it's kind of a bug to access the <code>T</code> inside without considering the new binders</p>



<a name="178683939"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683939" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683939">(Oct 21 2019 at 18:30)</a>:</h4>
<p>so it makes sense for it to be "owned"</p>



<a name="178683947"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683947" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683947">(Oct 21 2019 at 18:30)</a>:</h4>
<p>rustc is actually stricter on this point than chalk is, which is something I think we should improve</p>



<a name="178683951"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683951" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683951">(Oct 21 2019 at 18:30)</a>:</h4>
<p>well, I can't remember, actually</p>



<a name="178683966"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683966" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683966">(Oct 21 2019 at 18:30)</a>:</h4>
<p>at some point in rustc I had a branch that made the "value" of a <code>Binders</code> private</p>



<a name="178683976"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683976" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683976">(Oct 21 2019 at 18:31)</a>:</h4>
<p>so that all accesses to it had to go through some suitable API</p>



<a name="178683982"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683982" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683982">(Oct 21 2019 at 18:31)</a>:</h4>
<p>which made for easier auditing</p>



<a name="178683993"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178683993" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178683993">(Oct 21 2019 at 18:31)</a>:</h4>
<p>should prob do the same with chalk eventually</p>



<a name="178684048"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684048" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684048">(Oct 21 2019 at 18:31)</a>:</h4>
<p>ok, move on?</p>



<a name="178684055"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684055" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684055">(Oct 21 2019 at 18:31)</a>:</h4>
<blockquote>
<p>at some point in rustc I had a branch that made the "value" of a <code>Binders</code> private</p>
</blockquote>
<p>I remember doing that refactor in rustc, I believe it's still the case =)</p>



<a name="178684099"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684099" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684099">(Oct 21 2019 at 18:32)</a>:</h4>
<blockquote>
<p><a href="https://rust-lang.github.io/chalk/chalk_ir/struct.Binders.html" target="_blank" title="https://rust-lang.github.io/chalk/chalk_ir/struct.Binders.html">docs for Binders</a></p>
</blockquote>
<p>"Indicates that the value is universally quantified over N parameters of the given kinds, where N == self.binders.len(). A variable with depth i &lt; N refers to the value at self.binders[i]. Variables with depth &gt;= N are free."</p>



<a name="178684105"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684105" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684105">(Oct 21 2019 at 18:32)</a>:</h4>
<p>yeah, that's just wrong</p>



<a name="178684114"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684114" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684114">(Oct 21 2019 at 18:32)</a>:</h4>
<p>heh, awesome</p>



<a name="178684121"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684121" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684121">(Oct 21 2019 at 18:32)</a>:</h4>
<p>yeah I think I did a branch for it and then it bitrotted</p>



<a name="178684123"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684123" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684123">(Oct 21 2019 at 18:32)</a>:</h4>
<p>and then I made you do it :P</p>



<a name="178684195"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684195" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684195">(Oct 21 2019 at 18:33)</a>:</h4>
<blockquote>
<p>the basic rule that we want is that <code>dyn Foo: Foo</code> for any <code>Foo</code></p>
</blockquote>
<p>so this rule</p>



<a name="178684202"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684202" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684202">(Oct 21 2019 at 18:33)</a>:</h4>
<p>the question is, how do we handle this?</p>



<a name="178684212"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684212" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684212">(Oct 21 2019 at 18:33)</a>:</h4>
<blockquote>
<p>at some point in rustc I had a branch that made the "value" of a <code>Binders</code> private</p>
</blockquote>
<p>good thing you are restricting that for chalk now, otherwise i really would've just used that field to do computation upon</p>



<a name="178684218"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684218" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684218">(Oct 21 2019 at 18:33)</a>:</h4>
<p>in "old school chalk", we had a premise that we lowered all the impls/traits to a fixed set of program clauses</p>



<a name="178684251"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684251" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684251">(Oct 21 2019 at 18:33)</a>:</h4>
<p>but this doesn't work well for <code>dyn</code> and <code>impl</code> trait types</p>



<a name="178684255"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684255" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684255">(Oct 21 2019 at 18:33)</a>:</h4>
<p>because the set of rules is kind of open ended and huge</p>



<a name="178684305"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684305" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684305">(Oct 21 2019 at 18:34)</a>:</h4>
<p>especially once you consider things like <code>dyn Write + Send</code></p>



<a name="178684324"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684324" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684324">(Oct 21 2019 at 18:34)</a>:</h4>
<p>there we want two rules:</p>
<div class="codehilite"><pre><span></span><span class="n">dyn</span><span class="w"> </span><span class="p">(</span><span class="n">Write</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="nb">Send</span><span class="p">)</span>: <span class="nc">Write</span><span class="w"></span>
<span class="n">dyn</span><span class="w"> </span><span class="p">(</span><span class="n">Write</span><span class="w"> </span><span class="o">+</span><span class="w"> </span><span class="nb">Send</span><span class="p">)</span>: <span class="nb">Send</span>
</pre></div>



<a name="178684353"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684353" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684353">(Oct 21 2019 at 18:34)</a>:</h4>
<p>(note that chalk rules work with equality, not subtyping, so you can't just say <code>dyn Write: Write</code> -- and anyway <code>dyn (Write + Send)</code> is not a subtype of <code>dyn Write</code> in Rust)</p>



<a name="178684372"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684372" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684372">(Oct 21 2019 at 18:35)</a>:</h4>
<p>(which touches on the upcasting work that <span class="user-mention" data-user-id="124069">@Alexander Regueiro</span> has been pursuing :)</p>



<a name="178684429"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684429" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684429">(Oct 21 2019 at 18:35)</a>:</h4>
<p>however, the good thing is that chalk has been moving towards this more "on demand" model anyway</p>



<a name="178684457"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684457" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684457">(Oct 21 2019 at 18:36)</a>:</h4>
<p>which fits better with rust-analyzer, rustc, incremental, etc</p>



<a name="178684488"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684488" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684488">(Oct 21 2019 at 18:36)</a>:</h4>
<p>so basically there is this callback for the core engine where it says: </p>
<p>I have to prove the goal G, what are the relevant program clauses?</p>



<a name="178684499"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684499" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684499">(Oct 21 2019 at 18:36)</a>:</h4>
<p><span class="user-mention" data-user-id="125131">@detrumi</span> will remember this, as they did a lot of the core refactoring work here :)</p>



<a name="178684547"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684547" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684547">(Oct 21 2019 at 18:37)</a>:</h4>
<p>i'm a bit lost here, does a <code>QuantifiedWhereClause</code> have a corresponding <code>Goal</code>  definition associated with it?</p>



<a name="178684598"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684598" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684598">(Oct 21 2019 at 18:37)</a>:</h4>
<p>a "where clause" corresponds to a Rust where clause -- it is neither a goal nor a "clause"</p>



<a name="178684599"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684599" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684599">(Oct 21 2019 at 18:37)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> Speaking off which, how should we proceed with codegen?</p>



<a name="178684670"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684670" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684670">(Oct 21 2019 at 18:38)</a>:</h4>
<blockquote>
<p>a "where clause" corresponds to a Rust where clause -- it is neither a goal nor a "clause"</p>
</blockquote>
<p>let me glossary those:</p>



<a name="178684719"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684719" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684719">(Oct 21 2019 at 18:38)</a>:</h4>
<ul>
<li>goal -- something we are trying to prove</li>
<li>"clause" or "program clause" -- something we are assuming is true</li>
<li>where-clause (confusing!) -- bit of Rust syntax that sometimes has to be proven (and hence becomes a goal) and sometimes is assumed to be true (and hence a clause)</li>
</ul>



<a name="178684740"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684740" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684740">(Oct 21 2019 at 18:39)</a>:</h4>
<p>there is a collision of terminology here, which I hadn't fully realized, in that goal/clause come from prolog solvers</p>



<a name="178684775"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684775" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684775">(Oct 21 2019 at 18:39)</a>:</h4>
<p>and 'where clause' is just some thing I invented for <a href="https://rust-lang.github.io/rfcs/0135-where.html" target="_blank" title="https://rust-lang.github.io/rfcs/0135-where.html">RFC 135</a></p>



<a name="178684798"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684798" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684798">(Oct 21 2019 at 18:39)</a>:</h4>
<p><del>whichever one it was that introducd where clauses ;)</del> found it :)</p>



<a name="178684931"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684931" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684931">(Oct 21 2019 at 18:41)</a>:</h4>
<p>in particular though where clauses are a subset of goals etc</p>



<a name="178684935"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684935" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684935">(Oct 21 2019 at 18:41)</a>:</h4>
<p>(<span class="user-mention" data-user-id="124069">@Alexander Regueiro</span> -- let's discuss that later)</p>



<a name="178684950"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684950" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Alexander Regueiro <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684950">(Oct 21 2019 at 18:41)</a>:</h4>
<p>Okay</p>



<a name="178684957"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684957" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684957">(Oct 21 2019 at 18:41)</a>:</h4>
<blockquote>
<p>i'm a bit lost here, does a <code>QuantifiedWhereClause</code> have a corresponding <code>Goal</code>  definition associated with it?</p>
</blockquote>
<p>that is, you can convert a WC to a goal</p>



<a name="178684986"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178684986" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178684986">(Oct 21 2019 at 18:41)</a>:</h4>
<p>sorry, I feel like I'm rambling, not sure if I'm really answering your question <span class="user-mention" data-user-id="116108">@Keith Yeung</span></p>



<a name="178685050"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178685050" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178685050">(Oct 21 2019 at 18:42)</a>:</h4>
<p>(bikeshed: we could start calling them "where bounds" -- as opposed to "inline bounds"? but I don't want to derail further)</p>



<a name="178685100"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178685100" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178685100">(Oct 21 2019 at 18:42)</a>:</h4>
<p>i'm just wondering if a where-clause is a goal -- something that we want to prove</p>



<a name="178685111"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178685111" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178685111">(Oct 21 2019 at 18:42)</a>:</h4>
<blockquote>
<p>(bikeshed: we could start calling them "where bounds" -- as opposed to "inline bounds"? but I don't want to derail further)</p>
</blockquote>
<p>yeah, maybe</p>



<a name="178685129"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178685129" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178685129">(Oct 21 2019 at 18:43)</a>:</h4>
<p>I usually say "bound" to mean the thing on the right-hand side of a <code>:</code></p>



<a name="178685142"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178685142" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178685142">(Oct 21 2019 at 18:43)</a>:</h4>
<p>e.g., the <code>Debug</code> in <code>T: Foo</code> -- it's kind of a where-clause without the "self" part</p>



<a name="178685152"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178685152" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178685152">(Oct 21 2019 at 18:43)</a>:</h4>
<blockquote>
<p>i'm just wondering if a where-clause is a goal -- something that we want to prove</p>
</blockquote>
<p>ok -- well, the answer is "sometimes"</p>



<a name="178685159"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178685159" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178685159">(Oct 21 2019 at 18:43)</a>:</h4>
<p>e.g., </p>
<div class="codehilite"><pre><span></span><span class="k">fn</span> <span class="nf">foo</span><span class="o">&lt;</span><span class="n">T</span><span class="o">&gt;</span><span class="p">()</span><span class="w"> </span><span class="k">where</span><span class="w"> </span><span class="n">T</span>: <span class="nb">Send</span> <span class="p">{</span><span class="w">  </span><span class="p">}</span><span class="w"></span>
</pre></div>



<a name="178685177"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178685177" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178685177">(Oct 21 2019 at 18:43)</a>:</h4>
<p>when you call <code>foo</code>, you have to prove that <code>T: Send</code> for whichever value of <code>T</code> you chose (so it's a goal)</p>



<a name="178685186"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178685186" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178685186">(Oct 21 2019 at 18:43)</a>:</h4>
<p>but you type-check the <em>body</em> of <code>Foo</code>, you get to assume <code>T: Foo</code> for some placeholder <code>T</code> (so it's a "clause")</p>



<a name="178685258"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178685258" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178685258">(Oct 21 2019 at 18:44)</a>:</h4>
<blockquote>
<p>that is, you can convert a WC to a goal</p>
</blockquote>
<p>Isn't a WC context sensitive? Because it's just part of a type</p>



<a name="178685267"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178685267" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178685267">(Oct 21 2019 at 18:44)</a>:</h4>
<p>in the case of <code>dyn Send</code>, the same is true -- when you <em>create</em> an instance of a <code>dyn Send</code> type, you have to prove that <code>T: Send</code></p>



<a name="178685299"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178685299" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178685299">(Oct 21 2019 at 18:44)</a>:</h4>
<p>(but that sort of happens outside the purview of chalk)</p>



<a name="178685316"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178685316" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178685316">(Oct 21 2019 at 18:44)</a>:</h4>
<p>but when we are trying to prove <code>dyn Send: Send</code>, we get to assume things</p>



<a name="178685343"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178685343" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178685343">(Oct 21 2019 at 18:45)</a>:</h4>
<p>anyway let's talk through that exact mechanism a bit? maybe it becomes clearer?</p>



<a name="178685410"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178685410" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178685410">(Oct 21 2019 at 18:46)</a>:</h4>
<p>I'm trying to find the dang callback right now</p>



<a name="178685501"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178685501" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178685501">(Oct 21 2019 at 18:46)</a>:</h4>
<p>ok well there is this function:</p>



<a name="178685506"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178685506" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178685506">(Oct 21 2019 at 18:46)</a>:</h4>
<div class="codehilite"><pre><span></span><span class="k">pub</span><span class="p">(</span><span class="k">crate</span><span class="p">)</span><span class="w"> </span><span class="k">fn</span> <span class="nf">program_clauses_for_goal</span><span class="o">&lt;</span><span class="na">&#39;db</span><span class="o">&gt;</span><span class="p">(</span><span class="w"></span>
<span class="w">    </span><span class="n">db</span>: <span class="kp">&amp;</span><span class="na">&#39;db</span><span class="w"> </span><span class="n">dyn</span><span class="w"> </span><span class="n">RustIrDatabase</span><span class="p">,</span><span class="w"></span>
<span class="w">    </span><span class="n">environment</span>: <span class="kp">&amp;</span><span class="nc">Arc</span><span class="o">&lt;</span><span class="n">Environment</span><span class="o">&lt;</span><span class="n">ChalkIr</span><span class="o">&gt;&gt;</span><span class="p">,</span><span class="w"></span>
<span class="w">    </span><span class="n">goal</span>: <span class="kp">&amp;</span><span class="nc">DomainGoal</span><span class="o">&lt;</span><span class="n">ChalkIr</span><span class="o">&gt;</span><span class="p">,</span><span class="w"></span>
<span class="p">)</span><span class="w"> </span>-&gt; <span class="nb">Vec</span><span class="o">&lt;</span><span class="n">ProgramClause</span><span class="o">&lt;</span><span class="n">ChalkIr</span><span class="o">&gt;&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"> </span><span class="p">..</span><span class="w"> </span><span class="p">}</span><span class="w"></span>
</pre></div>



<a name="178685535"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178685535" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178685535">(Oct 21 2019 at 18:47)</a>:</h4>
<p><a href="https://github.com/rust-lang/chalk/blob/8abd14e1f0bb65dc95fdbbb87c12a95cc0063da1/chalk-solve/src/clauses.rs#L104-L113" target="_blank" title="https://github.com/rust-lang/chalk/blob/8abd14e1f0bb65dc95fdbbb87c12a95cc0063da1/chalk-solve/src/clauses.rs#L104-L113">from clauses.rs</a></p>



<a name="178685563"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178685563" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178685563">(Oct 21 2019 at 18:47)</a>:</h4>
<p>so what's happening here is that the solver is saying "I have to prove <code>goal</code>, what are the 'program clauses' I might use to do it"</p>



<a name="178685584"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178685584" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178685584">(Oct 21 2019 at 18:47)</a>:</h4>
<p>a program clause is just a clause that's globally true and widely know; perhaps a meaningless piece of jargon we should remove</p>



<a name="178685643"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178685643" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178685643">(Oct 21 2019 at 18:48)</a>:</h4>
<p>( it comes from prolog -- i.e., it's the clauses you wrote in your prolog program. )</p>



<a name="178685831"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178685831" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178685831">(Oct 21 2019 at 18:50)</a>:</h4>
<p>Huh, didn't know it was that simple</p>



<a name="178686194"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686194" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686194">(Oct 21 2019 at 18:54)</a>:</h4>
<p>anyway so the point is, suppose we are trying to prove something like</p>
<div class="codehilite"><pre><span></span><span class="n">dyn</span><span class="w"> </span><span class="n">Foo</span>: <span class="nc">XXX</span><span class="w"></span>
</pre></div>



<a name="178686211"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686211" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686211">(Oct 21 2019 at 18:54)</a>:</h4>
<p>or rather</p>



<a name="178686217"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686217" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686217">(Oct 21 2019 at 18:54)</a>:</h4>
<p>well, yes</p>



<a name="178686230"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686230" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686230">(Oct 21 2019 at 18:54)</a>:</h4>
<p>we are going to synthesize rules of the form <code>dyn Foo: Foo</code></p>



<a name="178686248"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686248" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686248">(Oct 21 2019 at 18:54)</a>:</h4>
<p>as possible clauses</p>



<a name="178686257"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686257" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686257">(Oct 21 2019 at 18:54)</a>:</h4>
<p>we are actually rather inefficient about this</p>



<a name="178686271"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686271" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686271">(Oct 21 2019 at 18:55)</a>:</h4>
<p>this is because we don't consider what the <code>XXX</code> is</p>



<a name="178686308"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686308" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686308">(Oct 21 2019 at 18:55)</a>:</h4>
<p>we just say "ah, you are trying to prove something of the form <code>dyn XXX: YYY</code>? I will make some rules like <code>dyn XXX: XXX</code> -- if it so happens that <code>XXX = YYY</code>, that would be useful to you; otherwise, it's not"</p>



<a name="178686321"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686321" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686321">(Oct 21 2019 at 18:56)</a>:</h4>
<p>this is ok because the callback is basically allowed to return "extra" rules that don't really apply to the goal at hand</p>



<a name="178686374"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686374" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686374">(Oct 21 2019 at 18:56)</a>:</h4>
<p>it should perhaps be improved at some point, but not imp't</p>



<a name="178686399"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686399" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686399">(Oct 21 2019 at 18:56)</a>:</h4>
<p>so where does that happen, you ask?</p>



<a name="178686418"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686418" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686418">(Oct 21 2019 at 18:56)</a>:</h4>
<p>in the function <a href="https://github.com/rust-lang/chalk/blob/8abd14e1f0bb65dc95fdbbb87c12a95cc0063da1/chalk-solve/src/clauses.rs#L135-L140" target="_blank" title="https://github.com/rust-lang/chalk/blob/8abd14e1f0bb65dc95fdbbb87c12a95cc0063da1/chalk-solve/src/clauses.rs#L135-L140"><code>program_clauses_that_could_match</code></a></p>



<a name="178686443"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686443" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686443">(Oct 21 2019 at 18:57)</a>:</h4>
<p>first we check if the thing you are trying to prove is <code>Implemented(TraitRef)</code> for some <code>TraitRef</code> (<a href="https://github.com/rust-lang/chalk/blob/8abd14e1f0bb65dc95fdbbb87c12a95cc0063da1/chalk-solve/src/clauses.rs#L142" target="_blank" title="https://github.com/rust-lang/chalk/blob/8abd14e1f0bb65dc95fdbbb87c12a95cc0063da1/chalk-solve/src/clauses.rs#L142">here</a>)</p>



<a name="178686462"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686462" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686462">(Oct 21 2019 at 18:57)</a>:</h4>
<p>in there <a href="https://github.com/rust-lang/chalk/blob/8abd14e1f0bb65dc95fdbbb87c12a95cc0063da1/chalk-solve/src/clauses.rs#L170-L183" target="_blank" title="https://github.com/rust-lang/chalk/blob/8abd14e1f0bb65dc95fdbbb87c12a95cc0063da1/chalk-solve/src/clauses.rs#L170-L183">we check if the self-type is <code>dyn Foo</code></a></p>



<a name="178686487"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686487" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686487">(Oct 21 2019 at 18:57)</a>:</h4>
<div class="codehilite"><pre><span></span><span class="w">            </span><span class="k">match</span><span class="w"> </span><span class="n">trait_ref</span><span class="p">.</span><span class="n">self_type_parameter</span><span class="p">()</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                </span><span class="nb">Some</span><span class="p">(</span><span class="n">Ty</span>::<span class="n">Opaque</span><span class="p">(</span><span class="n">qwc</span><span class="p">))</span><span class="w"> </span><span class="o">|</span><span class="w"> </span><span class="nb">Some</span><span class="p">(</span><span class="n">Ty</span>::<span class="n">Dyn</span><span class="p">(</span><span class="n">qwc</span><span class="p">))</span><span class="w"> </span><span class="o">=&gt;</span><span class="w"> </span><span class="p">{</span><span class="w"></span>
<span class="w">                    </span><span class="p">...</span><span class="w"></span>
<span class="w">                </span><span class="p">}</span><span class="w"></span>
<span class="w">                </span><span class="n">_</span><span class="w"> </span><span class="o">=&gt;</span><span class="w"> </span><span class="p">{}</span><span class="w"></span>
<span class="w">            </span><span class="p">}</span><span class="w"></span>
</pre></div>



<a name="178686559"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686559" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686559">(Oct 21 2019 at 18:58)</a>:</h4>
<p>here the <code>qwc</code> are those "quantified where clauses" we talked about before, so they have the type <code>Binder&lt;Vec&lt;Binder&lt;WhereClause&gt;&gt;&gt;</code></p>



<a name="178686565"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686565" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686565">(Oct 21 2019 at 18:58)</a>:</h4>
<p>really they are kind of "qqwc" -- quantified twice :)</p>



<a name="178686591"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686591" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686591">(Oct 21 2019 at 18:58)</a>:</h4>
<p>so if our goal were <code>dyn (Write + Send): Send</code> (say)</p>



<a name="178686627"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686627" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686627">(Oct 21 2019 at 18:59)</a>:</h4>
<p>then the self-type would be <code>dyn (Write + Send)</code>, and hence <code>qwc</code> would be something like</p>
<div class="codehilite"><pre><span></span>exists&lt;T&gt; { forall&lt;&gt; { T: Write }, forall&lt;&gt; { T: Send } }
</pre></div>



<a name="178686635"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686635" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686635">(Oct 21 2019 at 18:59)</a>:</h4>
<p>(where the <code>forall&lt;&gt;</code> indicates "empty" binders)</p>



<a name="178686718"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686718" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686718">(Oct 21 2019 at 19:00)</a>:</h4>
<p>what we want to produce are two program clauses:</p>
<div class="codehilite"><pre><span></span>dyn (Write + Send): Write
dyn (Write + Send): Send
</pre></div>



<a name="178686729"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686729" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686729">(Oct 21 2019 at 19:00)</a>:</h4>
<p>as it happens, only the second one will be useful for the goal at hand, but as I said, we don't consider that</p>



<a name="178686760"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686760" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686760">(Oct 21 2019 at 19:00)</a>:</h4>
<p>so we basically take the <code>qwc</code> and we substitute <code>dyn (Write + Send)</code> for that "self-type" <code>T</code></p>



<a name="178686769"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686769" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686769">(Oct 21 2019 at 19:00)</a>:</h4>
<div class="codehilite"><pre><span></span><span class="w">                    </span><span class="kd">let</span><span class="w"> </span><span class="n">self_ty</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">trait_ref</span><span class="p">.</span><span class="n">self_type_parameter</span><span class="p">().</span><span class="n">unwrap</span><span class="p">();</span><span class="w"> </span><span class="c1">// This cannot be None</span>
<span class="w">                    </span><span class="kd">let</span><span class="w"> </span><span class="n">wc</span><span class="w"> </span><span class="o">=</span><span class="w"> </span><span class="n">qwc</span><span class="p">.</span><span class="n">substitute</span><span class="p">(</span><span class="o">&amp;</span><span class="p">[</span><span class="n">self_ty</span><span class="p">.</span><span class="n">cast</span><span class="p">()]);</span><span class="w"></span>
</pre></div>



<a name="178686782"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686782" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686782">(Oct 21 2019 at 19:01)</a>:</h4>
<p>this gives us a value <code>wc</code> -- slightly misnamed, as these are actually still quantified where clauses</p>



<a name="178686814"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686814" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686814">(Oct 21 2019 at 19:01)</a>:</h4>
<p>so <code>wc</code> would be</p>
<div class="codehilite"><pre><span></span> vec![
    forall&lt;&gt; { (dyn Write + Send): Write },
    forall&lt;&gt; { dyn (Write + Send): Send }
]
</pre></div>



<a name="178686874"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686874" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686874">(Oct 21 2019 at 19:02)</a>:</h4>
<p>on the final line we convert those into program clauses by using the <code>cast()</code> function</p>



<a name="178686881"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686881" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686881">(Oct 21 2019 at 19:02)</a>:</h4>
<div class="codehilite"><pre><span></span><span class="w">                    </span><span class="n">clauses</span><span class="p">.</span><span class="n">extend</span><span class="p">(</span><span class="n">wc</span><span class="p">.</span><span class="n">into_iter</span><span class="p">().</span><span class="n">casted</span><span class="p">());</span><span class="w"></span>
</pre></div>



<a name="178686888"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686888" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686888">(Oct 21 2019 at 19:02)</a>:</h4>
<p>argh, I ust realized it's 3pm ..</p>



<a name="178686891"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686891" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686891">(Oct 21 2019 at 19:02)</a>:</h4>
<p>sorry, I gotta run to another mtg :)</p>



<a name="178686909"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686909" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686909">(Oct 21 2019 at 19:02)</a>:</h4>
<p>sorry for the occasional delay today, I had some "local" interruptions</p>



<a name="178686918"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178686918" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178686918">(Oct 21 2019 at 19:03)</a>:</h4>
<p>anyway, I'll try to answer questions async, hope that was helpful so far to explain what <span class="user-mention" data-user-id="116108">@Keith Yeung</span> did :)</p>



<a name="178687047"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178687047" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178687047">(Oct 21 2019 at 19:04)</a>:</h4>
<p>I thought it was helpful, thanks</p>



<a name="178687080"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178687080" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178687080">(Oct 21 2019 at 19:04)</a>:</h4>
<p>also, it might be worth taking your "more general" example here and adding it as a comment in the implementation</p>



<a name="178687244"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178687244" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178687244">(Oct 21 2019 at 19:06)</a>:</h4>
<p>as a reminder of why we're working with a vec of clauses, for instance</p>



<a name="178687455"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178687455" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178687455">(Oct 21 2019 at 19:09)</a>:</h4>
<p>Ooh, so we're substituting the <code>T</code>, and that removes the <code>exists&lt;T&gt;</code>, leaving us with a vec instead. Was wondering where the vec came from</p>



<a name="178687561"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178687561" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> tmandry <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178687561">(Oct 21 2019 at 19:10)</a>:</h4>
<p>(I would make the docs/comments changes myself but I also have to run)</p>



<a name="178687562"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178687562" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> detrumi <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178687562">(Oct 21 2019 at 19:10)</a>:</h4>
<p>That's a lot of implicit steps</p>



<a name="178694866"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178694866" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178694866">(Oct 21 2019 at 20:25)</a>:</h4>
<blockquote>
<p>(I would make the docs/comments changes myself but I also have to run)</p>
</blockquote>
<p>yep I was thinking the same</p>



<a name="178694869"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178694869" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178694869">(Oct 21 2019 at 20:25)</a>:</h4>
<p>I'll open a small PR</p>



<a name="178705339"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178705339" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178705339">(Oct 21 2019 at 22:30)</a>:</h4>
<p><span class="user-mention" data-user-id="116009">@nikomatsakis</span> I was thinking that trait solving for <code>dyn Trait</code> is not the same as <code>impl Trait</code></p>



<a name="178705357"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178705357" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178705357">(Oct 21 2019 at 22:30)</a>:</h4>
<p>they seem to have different rules as I understand it</p>



<a name="178705479"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178705479" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178705479">(Oct 21 2019 at 22:32)</a>:</h4>
<p>namely, <code>dyn Trait</code> doesn't <em>just</em> mean <code>exists&lt;T&gt; { forall&lt;&gt; { T: Trait } }</code>, it also carries an assumption that the T is behind a pointer</p>



<a name="178705609"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178705609" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Keith Yeung <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178705609">(Oct 21 2019 at 22:34)</a>:</h4>
<p>although on second thought, that doesn't seem to be a concern, since all chalk needs to do is to generate another goal to prove that <code>dyn Trait: Pointee</code> or something</p>



<a name="178712540"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/meeting%202019-10-21/near/178712540" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> nikomatsakis <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/meeting.202019-10-21.html#178712540">(Oct 22 2019 at 00:30)</a>:</h4>
<blockquote>
<p>namely, <code>dyn Trait</code> doesn't <em>just</em> mean <code>exists&lt;T&gt; { forall&lt;&gt; { T: Trait } }</code>, it also carries an assumption that the T is behind a pointer</p>
</blockquote>
<p>indeed I don't think this is really chalk's concern; there <em>are</em> some interactions with the <code>Sized</code> trait</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>